diff --git a/IMPLEMENTATION_PLAN.md b/IMPLEMENTATION_PLAN.md index 7cac553..653a7aa 100644 --- a/IMPLEMENTATION_PLAN.md +++ b/IMPLEMENTATION_PLAN.md @@ -17,6 +17,18 @@ priorities. > below). What remains is the downstream Netclaw integration, which needs > actions outside this repository. +- [ ] **v0.3 authored-command approval correction.** Treat PowerShell and Bash + approval completeness consistently: prove every authored executable + region, but do not require proof of ambient aliases, functions, modules, + profiles, executable lookup, or inherited environment state. Preserve the + existing `PwshInitialStateMode` API. Next update default-mode PowerShell + occurrence completeness while keeping loop-dependent effective values + Unknown unless fresh-process state is proved, expand the executable + corpus, and prove the Netclaw approval matrix. Explicit + source mutation, computed identity, hidden execution, unknown receiver + semantics, unsupported constructs, and policy-sensitive unknown values, + paths, cwd, or redirects remain strict. + ### Implemented (SPEC.POWERSHELL.md §16 phases 1–14) — done - [x] **1. Public-API surface** — `ShellParserOptions` base; `BashParserOptions` @@ -285,9 +297,9 @@ priorities. 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 + retain explicit native/script binding candidates only when the alpha.3 + 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 @@ -295,10 +307,12 @@ priorities. 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. + pipelines fail atomically. Alpha.3 authorization completeness requires + the explicit constrained command-resolution baseline, including after + decoded-host boundaries. The v0.3 authored-command approval correction + above supersedes that behavior and is pending implementation. + 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 @@ -402,18 +416,18 @@ priorities. projects iterator and loop-body ancestry, survives decoded wrappers, and fails closed on dynamic iterables, iterator/body state or command-resolution mutation, malformed boundaries, and depth overflow. - Loop-body and current-scope post-loop occurrences intentionally remain - incomplete; isolated child-host loops do not taint their outer continuation. - Before publishing exact or finite values, add an explicit PowerShell - 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. 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`. The first - value-analysis pass now consumes that contract, retains parser-owned + Alpha.3 leaves default-mode loop-body and current-scope post-loop + occurrences incomplete; the authored-command correction will make static + occurrences complete without weakening explicit mutation or dynamic + execution checks. Isolated child-host loops do not taint their outer + continuation. + Alpha.3 added an explicit PowerShell initial-runspace contract and + wrapper-state metadata. The additive `PwshInitialStateMode` API remains + locked. The v0.3 authored-command correction no longer requires isolated + mode for static command completeness and removes its old pinned-module + implication; loop-dependent effective values still require the fresh- + process assertion. The first value-analysis pass consumes that contract, + retains parser-owned argument provenance, proves quoted scalar and literal-array domains, retains ordered duplicate visits separately from public set summaries, guards a pinned documented preference inventory plus fresh-host built-ins diff --git a/PROJECT_CONTEXT.md b/PROJECT_CONTEXT.md index 4295f28..8528964 100644 --- a/PROJECT_CONTEXT.md +++ b/PROJECT_CONTEXT.md @@ -91,6 +91,11 @@ zero-native-deps .NET parser sized to what security gates actually need. 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. +- Define occurrence completeness over authored executable syntax for both + shells. Ambient aliases, functions, modules, profiles, executable lookup, + inherited variables, and other host externalities do not make static authored + commands incomplete. Explicit mutations and hidden or computed execution in + the submitted source remain fail closed. - Deliver Bash `for ... in` and PowerShell `foreach` in stable v0.3. Condition loops, branches, and shared-analysis extraction are post-v0.3 work and do not gate the validating consumer migration. diff --git a/SPEC.POWERSHELL.md b/SPEC.POWERSHELL.md index f9a2d80..c3dfeae 100644 --- a/SPEC.POWERSHELL.md +++ b/SPEC.POWERSHELL.md @@ -115,7 +115,7 @@ public abstract record ShellParserOptions /// = ... }` still compiles. public sealed record BashParserOptions : ShellParserOptions; -/// Declares which ambient PowerShell runspace facts the caller can prove. +/// Compatibility option for PowerShell initial host-state analysis. public enum PwshInitialStateMode { Unknown, @@ -419,55 +419,42 @@ direct execution region, cataloged execution-bearing argument, or conservative unknown-receiver region. A proved non-executing 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, read-only, -typed, validated, preference, or configuration variables are eligible. -Scoped/provider bindings such as `$global:x`, `$script:x`, `$private:x`, and -`$env:X` fail the loop region closed. A built-in or ambient binding therefore -cannot coerce, reject, or otherwise alter a value the analyzer presents as an -exact string, or change host behavior as a side effect of loop assignment. -The supported preference-variable inventory is pinned to PowerShell's -`about_Preference_Variables` reference rather than inferred only from variables -materialized by a fresh host; lazy and configuration-dependent names remain -ineligible even when `Get-Variable` does not initially enumerate them. +`PwshInitialStateMode.Unknown` remains the default and does not publish exact or +finite loop-dependent effective values. An ambient typed, validated, read-only, +or constant binding may coerce or reject the assignment, so authored iterable +text is not a proved runtime argument. The surrounding static command +occurrence may still be complete because value precision is independent. + +`IsolatedNonInteractiveNoProfile` asserts that the complete source runs in a +newly spawned noninteractive PowerShell process with profiles disabled and no +reused or caller-initialized runspace. It permits exact or finite values for +ordinary unscoped bindings. It does not assert a pinned module, alias, function, +`PATH`, or executable-resolution baseline; those runtime externalities are +outside authored-command completeness. + +Only ordinary unscoped binding names that do not case-insensitively collide +with PowerShell's automatic, constant, read-only, preference, or configuration +variables are eligible. Scoped/provider bindings such as `$global:x`, +`$script:x`, `$private:x`, and `$env:X` fail the loop region closed. These +special names are visible in the submitted source and can change host behavior. +Typed and validated ambient bindings are the reason default-mode effective +values stay `Unknown`; the parser never reports authored text as a proved +runtime value when coercion or rejection is possible. 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. -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. +current runspace and share supported authored binding and location state. +Decoded `pwsh -Command` and `pwsh -EncodedCommand` payloads do not inherit exact +`$HOME`, environment, provider, or cwd facts unless those facts are +independently proved. They do retain complete static authored command +occurrences. Path-shaped native or `.ps1` spellings use their authored binding +classification; ambient alias, function, module, profile, and executable +resolution is outside the approval-grammar proof. + +Recognized source-level variable, alias, function, or module mutation +invalidates later affected proofs in every observing scope. A computed or +otherwise hidden invocation remains incomplete and may invalidate later state; +an unmodeled explicit pipeline writer fails atomically. Cwd-only mutation +retains independent authored-binding facts. Mutation is recognized from the effective parameter vector as well as the verb. Common parameter writers `-OutVariable` / `-ov`, `-PipelineVariable` / @@ -543,10 +530,11 @@ The version-pinned PowerShell 7 catalog covers: | `Start-Job -ScriptBlock` | Main | Concurrent | Once | child process; exit isolated | | `New-Module -ScriptBlock` | Initialization | Synchronous | Once | module state; current-runspace effects analyzed separately | -Remote `Invoke-Command` bodies begin with Unknown working directory, bindings, -aliases, functions, modules, profiles, and command resolution. Local parser -state is not an inheritance proof for a remote host or persistent session, and -remote exit state never flows into the invoking host continuation. A complete +Remote `Invoke-Command` bodies begin with Unknown working directory and +host-dependent values. Their static authored command occurrences remain +complete; local parser state is not an inheritance proof for a remote host or +persistent session, and remote exit state never flows into the invoking host +continuation. A complete literal, quoted, URI, GUID, or hashtable target proves one activation. A complete top-level comma-separated target list, whether named, inline, or positional, proves concurrent scheduling but maps to public cardinality @@ -584,11 +572,11 @@ fails atomically. 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. +Catalog lookup classifies the authored command for approval; it is not a claim +about ambient runtime resolution. A catalog entry may classify a script block +as non-executing data unless an explicit source-level mutation has invalidated +that authored receiver proof. 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 @@ -598,9 +586,8 @@ runtime order. Variable, location, command-resolution, runspace, and process propagation are analyzed independently. Cataloged receivers may retain already-proved scheduling facts without making further catalog expansion release-gating. -Unproved receiver, binding, or state facts remain Unknown rather than borrowing -registration-time state. A -constrained canonical `Write-Output { Remove-Item x }` +Unproved receiver, binding, or authored state facts remain Unknown rather than +borrowing runtime state. A static authored `Write-Output { Remove-Item x }` remains opaque data and does not invent a `Remove-Item` occurrence. A leading `param(...)` declaration inside any execution region remains outside @@ -1199,9 +1186,9 @@ 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. +mode. Native-versus-cmdlet path interpretation uses the authored command +spelling and parser tables; ambient runtime shadowing does not erase that +classification. An explicit source-level mutation may invalidate it. When every fragment, transformation, binding fact, cwd/home fact, and consumer fact is exact, mixed literal and expandable fragments compose to one @@ -1461,9 +1448,9 @@ lists, pipelines, loops, groups, and substitutions, including built-in cmdlets such as `Tee-Object` whose verb is not in the approved-verb table. The supported module-qualified exceptions are `Microsoft.PowerShell.Utility\Invoke-Expression` and the version-pinned §4 -execution-region receiver catalog under its constrained command-resolution -contract. A quoted string is a command -identity only when preceded by the call operator `&`; otherwise it is an +execution-region receiver catalog under its authored-receiver contract. A +quoted string is a command identity only when preceded by the call operator +`&`; otherwise it is an unsupported expression. Any dynamic command identity invalidates following location attribution because it can resolve to current-scope code that calls `Set-Location`. diff --git a/SPEC.md b/SPEC.md index 8f5da30..ab79bc9 100644 --- a/SPEC.md +++ b/SPEC.md @@ -123,7 +123,7 @@ public sealed record BashParserOptions : ShellParserOptions public BashInitialStateMode InitialStateMode { get; init; } } -/// Declares which ambient PowerShell runspace facts the caller can prove. +/// Compatibility option for PowerShell initial host-state analysis. public enum PwshInitialStateMode { Unknown, @@ -299,62 +299,49 @@ 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 variable state. Exact and finite -binding proofs remain limited to ordinary unscoped variable names that do not -collide, case-insensitively, with automatic, constant, read-only, typed, -validated, preference, or configuration bindings known to the supported -PowerShell runtime. A `foreach` assignment to a built-in preference variable -can coerce an authored string into an enum or reject it, and can change host -behavior independently of the loop value; it is therefore not an ordinary -string binding. Documented preference names remain excluded even when they are -lazy or configuration-dependent and therefore absent from a fresh -`Get-Variable` inventory. 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. +`PwshInitialStateMode.Unknown` is the default. PowerShell authorization uses +the same boundary as Bash authorization: it proves the static authored command +and every authored executable region, not the runtime implementation selected +through aliases, functions, modules, profiles, executable lookup, inherited +variables, or other ambient host state. Ambient uncertainty alone therefore +does not make a static command occurrence incomplete and does not poison later +authored command occurrences. + +`PwshInitialStateMode.Unknown` does not publish an exact or finite +loop-dependent effective value. An ambient typed, validated, read-only, or +constant binding may coerce or reject an assignment, so the authored iterable +text is not a proved runtime argument. The surrounding static command +occurrence may still be complete; value precision is a separate fact. + +`PwshInitialStateMode.IsolatedNonInteractiveNoProfile` is a caller assertion +that the complete source runs in a newly spawned noninteractive PowerShell +process with profiles disabled and without a reused or caller-initialized +runspace. It permits exact or finite loop-dependent values for ordinary +unscoped names. It does not assert a pinned module, alias, function, `PATH`, or +executable-resolution baseline, because those runtime externalities are outside +authored-command completeness. + +The bounded grammar remains limited to ordinary unscoped variable names that +do not collide, case-insensitively, with automatic, constant, read-only, +preference, or configuration bindings known to the supported PowerShell +runtime. Scoped/provider forms such as `$global:x`, `$script:x`, and `$env:X` +remain outside the bounded loop-binding grammar. + 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`. -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 -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. +`Invoke-Expression` payload share supported authored binding and location +state. A decoded `pwsh -Command` or `pwsh -EncodedCommand` child does not +inherit exact `$HOME`, environment, provider, or cwd facts unless those facts +are independently proved, but it retains complete static authored command +occurrences. Explicit native, `.ps1`, cmdlet, alias, and module-qualified +spellings use their authored parser classification even though runtime state +may shadow them. + +Recognized source-level mutation of variables, aliases, functions, or modules +invalidates later affected proofs wherever PowerShell scope rules make the +mutation observable. A computed `Invoke-Expression` payload can hide commands +and mutate current-runspace facts; it therefore invalidates later binding and +cwd proofs and remains incomplete. Cwd-only state changes retain independent +authored-binding facts. Variable mutation recognition includes argument-vector binding, not only the invoked verb. The PowerShell common parameters `-OutVariable` / `-ov`, @@ -671,6 +658,16 @@ public static class ShellAnalysisLimits } ``` +`IsComplete` proves that the parser discovered the complete authored +executable region, assigned its structural ancestry, and completed every +parser-owned authored-syntax check. It does not prove which runtime executable +an ambient alias, function, module, profile, `PATH`, or inherited environment +will select. Static authored command identities remain complete under that +external uncertainty. Computed identities, hidden executable text, and +unsupported regions remain incomplete or make the whole result unparseable. +After an explicit source-level mutation that the parser cannot model, affected +later identities or values remain incomplete. + `Commands` contains one entry per authored simple command that may execute, not one per predicted runtime iteration. `Ancestry` is ordered outermost to innermost, excludes the simple-command leaf, and retains every enclosing @@ -825,7 +822,8 @@ unwraps statically proved `command` and `builtin` dispatch; dynamic or invalid wrapper grammar fails closed. Ordinary `printf` without `-v` remains supported. -Command-resolution state is independent from variable attributes and cwd. +Authored command-resolution mutation is independent from variable attributes +and cwd. `exec` fails the complete parse closed globally because it replaces the shell or makes commandless redirections persistent. Mutating or ambiguous `hash`, `alias`, `unalias`, `shopt`, and `enable` forms likewise fail globally before a @@ -2656,10 +2654,12 @@ What a v0.3 Netclaw-style security consumer expects from this library: 2. The consumer evaluates every `CommandOccurrence`, including condition, iterator, branch, body, substitution, and pipeline-stage occurrences. `Syntax` may group the UI but is not the command-discovery API. -3. An incomplete occurrence, dynamic verb, unknown or unrecognized role, +3. An incomplete occurrence, dynamic authored verb, unknown or unrecognized role, ancestry kind, value kind, redirect kind, or policy-sensitive fact prompts or denies. Unknown executable operands are never dropped to reuse a broader - approval. + approval. Ambient runtime resolution does not by itself make a static + authored occurrence incomplete; the approval covers the command text the + user was shown. 4. For every exact or finite effective value, the consumer reapplies the shell's binding rules and the complete executable-specific grammar at the candidate's authored position. A finite shell proof is not authorization; diff --git a/docs/CONSUMER_GUIDE.md b/docs/CONSUMER_GUIDE.md index 36a9347..5cc10e4 100644 --- a/docs/CONSUMER_GUIDE.md +++ b/docs/CONSUMER_GUIDE.md @@ -202,6 +202,13 @@ installed prerelease remain prompt-or-deny cases. The migration rules are: scope, cwd, or redirects. A structurally complete occurrence may still have an unknown value; those are separate facts. +This authorization is about authored shell syntax. `IsComplete` means the +parser found and classified every executable region in the submitted command; +it does not promise which runtime executable an ambient alias, function, +module, profile, `PATH`, or inherited environment will select. Netclaw-style +gates show the submitted command to the user and authorize that visible command. +They are not responsible for reconstructing every externality in the host. + Bash loop-variable proofs also require an execution-environment assertion. `BashInitialStateMode.Unknown` is the safe default and makes a bounded `for` region unparseable: the parser cannot discover whether an ambient variable is @@ -243,21 +250,18 @@ 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 authorization proofs require the parallel but shell-specific -assertion. `PwshInitialStateMode.Unknown` is the safe default: the parser can -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 -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: +PowerShell follows the same authored-command boundary. The safe default is +`PwshInitialStateMode.Unknown`, and ordinary static commands remain complete in +that mode. Ambient aliases, functions, modules, profiles, executable lookup, +and other host state do not make every visible command dynamic. A +loop-dependent effective value remains `Unknown` in default mode because an +ambient typed or validated variable can coerce or reject the assignment. + +Select `IsolatedNonInteractiveNoProfile` only when the complete source runs in +a newly spawned noninteractive PowerShell process with profiles disabled and no +reused or caller-initialized runspace. That assertion permits exact or finite +ordinary literal `foreach` values. It does not require pinned modules or a +reviewed command-resolution baseline: ```csharp var parser = new PwshParser(new PwshParserOptions @@ -267,15 +271,21 @@ 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 -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. +Static-command approval reuse based on `ParsedCommand.Commands` does not +require the isolated mode. A decoded child host keeps complete static authored commands, but it does +not inherit exact environment, home, provider, or cwd facts that were not +independently proved. `( ... )`, `$()`, and static `Invoke-Expression` share +current-runspace authored state. Never select isolated mode merely to suppress +approval prompts. + +The parser still treats facts visible in the submitted source as security +boundaries. Computed invocation such as `& $exe`, computed +`Invoke-Expression`, hidden executable text, explicit alias/function/module +mutation, unsupported constructs, and unknown script-block receiver semantics +remain incomplete or unparseable. Hard-deny and protected-path checks still run +before approval reuse. Unknown values, paths, cwd, and redirects remain strict +when they affect policy even if the surrounding command occurrence is +structurally complete. Under the stable v0.3 contract, heredoc and Bash here-string bodies are stdin data, not implicit child commands or filesystem paths. Authorize any command @@ -359,6 +369,11 @@ redirect target remains unknown, so test all of these facts separately. ## Choosing a command identity +Choose the identity from the authored syntax. Runtime command discovery is an +executor concern. A consumer does not need to enumerate profiles, modules, +aliases, functions, or `PATH` before it can ask the user to approve the command +that will be submitted to the shell. + For PowerShell aliases, prefer the canonical cmdlet identity while retaining the token the user typed for display: @@ -592,8 +607,9 @@ static bool IsKnownRedirectOperation(RedirectOperation operation) => 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')) { +target, so path policy still prompts. Under an isolated fresh-process +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. @@ -632,9 +648,9 @@ 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. +the decoded child has unknown host-dependent values. A static decoded child +command remains a complete authored occurrence. 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 diff --git a/openspec/changes/v0-3-structured-shell-analysis/design.md b/openspec/changes/v0-3-structured-shell-analysis/design.md index 4675bef..802c496 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/design.md +++ b/openspec/changes/v0-3-structured-shell-analysis/design.md @@ -342,9 +342,8 @@ Execution-bearing script blocks bound to that command are owned separately by an authored-order `ExecutionRegions` collection. The unchanged `Clause` keeps the script-block token as an opaque `DynamicSkip` argument for compatibility; the execution-region node records why and how the block may run. A script block -proved to be data, such as the argument to canonical `Write-Output` in a -constrained command-resolution context, remains only the opaque argument and -does not gain a region. +proved to be data from its static authored receiver, such as the argument to +`Write-Output`, remains only the opaque argument and does not gain a region. ### Model PowerShell execution regions without a false scope union @@ -405,10 +404,10 @@ wildcards, and set overflow collapse to all unproved command names. This prevents both an alias to `Set-Item` and a rebound `Set-Alias` mutator from hiding an environment-provider write without tainting unrelated names. -Remote `Invoke-Command` does not reuse local cwd, binding, alias, function, -module, profile, or command-resolution facts. The remote body is always -authorization-visible but incomplete under that arbitrary initial state, and -its exit state never affects the invoking host continuation. A complete single +Remote `Invoke-Command` does not reuse local cwd or host-dependent value facts. +Static commands in the remote body remain complete authored occurrences even +though their runtime resolution and ambient environment are external. Remote +exit state never affects the invoking host continuation. A complete single target proves synchronous/once execution. A complete top-level multiple-target list, an enabled `-AsJob`, or an enabled `-InDisconnectedSession` proves concurrent execution; quoted, escaped, or nested commas remain scalar, and @@ -436,11 +435,10 @@ incomplete facts; an unproved interior pipeline fails atomically. 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. +Catalog lookup proves the authored receiver classification, not ambient runtime +resolution. A catalog entry may keep a script block as data unless bounded +source-level mutation provenance shows that the authored spelling or its known +canonical alias target was changed earlier in the submitted source. An unknown receiver or ambiguous binding is over-approximated as an execution region with unknown facts. Commands in a supported non-pipeline body remain @@ -604,47 +602,43 @@ ordinary command identities; `command time ...` does not invent reserved-word semantics. The structured Bash BNF therefore does not include a `bash_group` production until brace-group support is actually implemented. -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, read-only, -typed, validated, preference, or configuration variables known to the -supported runtime. Built-in preference variables are excluded because -assignment can coerce or reject authored strings or alter host behavior. The -reviewed documented inventory is pinned independently from the live fresh-host -oracle so lazy and configuration-dependent preferences cannot escape the gate. -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. -Path-shaped command spellings remain candidates rather than immutable binding -proofs because PowerShell aliases can shadow explicit native and `.ps1` names. -Decoded children also clear automatic `$HOME` and environment-value facts -because an uncontrolled profile can mutate them before the payload; configured -provider/native tilde initialization remains independent. Default ambient -uncertainty preserves ordinary v0.2 completeness and does not count as an -observed mutation, while binding-dependent effective values remain Unknown. -Recognized -variable, alias, -function, or module mutation invalidates every later observing proof; a cwd-only -transfer preserves the independent initial-runspace assertion. A computed -`Invoke-Expression` can perform any of those mutations in the current runspace, -so it invalidates later bindings and command resolution and makes cwd unknown; -inside an unmodeled loop transfer it fails the complete region atomically. +PowerShell uses the same authored-command approval boundary as Bash. A static +command spelling proves the authored identity used for approval; it does not +prove which executable, alias, function, cmdlet, module export, or script the +runtime will select. Profiles, module auto-loading, `PATH`, inherited variables, +and other ambient host facts are executor externalities rather than reasons to +mark every visible command incomplete. This is an intentional product boundary: +the approval gate shows the submitted shell command and asks whether that +authored command is permitted. + +`PwshParserOptions.InitialStateMode` remains in the public API for compatibility +and is not a precondition for a complete static command occurrence. Default +mode still withholds exact or finite loop-dependent effective values: an +ambient typed or validated binding can coerce or reject the assignment, so +authored iterable text is not a proved runtime argument. + +`IsolatedNonInteractiveNoProfile` asserts a newly spawned noninteractive, +no-profile PowerShell process with no reused or caller-initialized runspace. It +permits exact or finite values for ordinary unscoped loop bindings without +claiming a pinned module, alias, function, `PATH`, or executable-resolution +baseline. The positive binding grammar still excludes automatic, constant, +read-only, preference, configuration, scoped, and provider names whose special +semantics are visible in the submitted source. + +Current-runspace groups, `$()`, and static `Invoke-Expression` share supported +authored binding and cwd state. Decoded children do not inherit exact `$HOME`, +environment, provider, or cwd facts unless those values are independently +proved, but ambient uncertainty does not invalidate their static authored +command identities. Native, `.ps1`, cmdlet, alias, and module-qualified +spellings are classified from their authored syntax and the parser's versioned +tables; runtime shadowing is outside this proof. + +Explicit source-level variable, alias, function, or module mutation remains in +scope. A later affected occurrence or value stays incomplete unless the parser +can model the mutation exactly. A computed `Invoke-Expression` can hide commands +and mutate current-runspace state, so it invalidates later bindings and cwd and +fails an unmodeled loop transfer atomically. Cwd-only transfer retains the +independent authored-binding facts. Effective values are shell facts, not executable semantics. The analysis must preserve both the authored shell classification and each proved effective @@ -756,14 +750,13 @@ Provider-capable item mutators invalidate binding proofs when a scalar, array, subexpression, or variable target cannot be proved outside a mutable state provider. Target-position tracking avoids treating a dynamic value as a state target when the filesystem path itself is proved. -An independent observed-mutation bit invalidates command identity for every -later ordinary or loop occurrence. It is not inferred merely from the default -ambient-state mode, so state is not invalidated before the first occurrence and -the v0.2 compatibility leaves remain visible. A v0.3 authorization occurrence -is nevertheless incomplete until the caller supplies the constrained -command-resolution baseline. Once reached, an unproved invocation may be -arbitrary in-process code and therefore invalidates subsequent observable -state. If it is a pipeline stage, the existing fail-atomic pipeline-writer rule +An independent observed-mutation bit invalidates affected authored binding or +receiver proofs after an explicit source-level mutation. It is never inferred +from ambient state or from an otherwise static unknown command, so ordinary +authored occurrences remain complete and do not poison following state merely +because runtime resolution is external. A computed invocation or an invocation +with hidden executable syntax remains incomplete. If an explicit unmodeled +writer is a pipeline stage, the existing fail-atomic pipeline-writer rule applies until inter-stage state propagation is modeled. The PowerShell 7 mutation inventory includes `Import-Alias` and `Import-PSSession` because they can clobber existing command names, and diff --git a/openspec/changes/v0-3-structured-shell-analysis/proposal.md b/openspec/changes/v0-3-structured-shell-analysis/proposal.md index 658f382..b1aa288 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/proposal.md +++ b/openspec/changes/v0-3-structured-shell-analysis/proposal.md @@ -19,6 +19,12 @@ fail-closed behavior for incomplete analysis. - Add a library-owned command-occurrence projection containing every command that may execute in supported grammar, including iterator, loop-body, wrapped, substitution, and PowerShell script-block execution-region commands. +- Define authorization completeness over authored shell syntax. A complete + occurrence proves that the parser discovered and classified the submitted + executable region; it does not prove the runtime executable selected by + aliases, functions, modules, profiles, `PATH`, or other ambient host state. + Consumers authorize the visible authored command and keep runtime command + resolution outside the grammar proof boundary for both Bash and PowerShell. - Correct the PowerShell script-block boundary: represent direct invocation, current-runspace callbacks, child-runspace/process jobs, module initialization, and unknown receivers as typed execution regions while @@ -74,6 +80,10 @@ fail-closed behavior for incomplete analysis. does not hide commands. - Keep executable-specific option and operand interpretation, authorization policy, and durable approval scope consumer-owned. +- Keep ambient runtime command resolution and other executor externalities + consumer- and host-owned. Explicit source-level mutations, computed command + identities, hidden execution, and unsupported constructs remain parser-owned + fail-closed boundaries. - Update `docs/CONSUMER_GUIDE.md` and the README usage path so security gates authorize the complete command-occurrence projection and use the syntax tree only for structure, display, and specialized analysis. diff --git a/openspec/changes/v0-3-structured-shell-analysis/specs/bounded-shell-analysis/spec.md b/openspec/changes/v0-3-structured-shell-analysis/specs/bounded-shell-analysis/spec.md index 732748a..b0f86c1 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/specs/bounded-shell-analysis/spec.md +++ b/openspec/changes/v0-3-structured-shell-analysis/specs/bounded-shell-analysis/spec.md @@ -119,12 +119,12 @@ retain their existing meanings. - **THEN** `-LiteralPath` still applies quoted tilde, provider-qualifier, and PSDrive semantics - **THEN** the parser does not enumerate the filesystem for any form -#### Scenario: Path-shaped PowerShell command names remain shadowable -- **WHEN** isolated-mode PowerShell parses an explicit native or `.ps1` path command before any command-resolution mutation -- **THEN** its spelling may supply the candidate native-versus-PowerShell argument-binding semantics -- **WHEN** a matching alias mutation has been observed, or the command executes in an unconstrained decoded child -- **THEN** path spelling alone does not prove command identity or argument-binding semantics -- **THEN** a shell-sensitive effective value remains Unknown +#### Scenario: Path-shaped PowerShell commands use authored semantics +- **WHEN** PowerShell parses an explicit native or `.ps1` path command +- **THEN** its spelling supplies the authored native-versus-PowerShell argument-binding semantics +- **THEN** ambient aliases, functions, modules, profiles, and executable lookup do not make the occurrence incomplete +- **WHEN** a matching source-level command-resolution mutation has been observed +- **THEN** later affected binding semantics remain incomplete unless the mutation is modeled exactly #### Scenario: Decoded host profiles can mutate home facts - **WHEN** isolated-mode PowerShell decodes a child `pwsh -Command` or `-EncodedCommand` payload that references `$HOME` or `$env:USERPROFILE` @@ -304,43 +304,40 @@ reserved syntax. - **WHEN** Bash parses `coproc exec /bin/rm target.txt` - **THEN** the whole result is unparseable until coprocess structure and timing are modeled -### 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, read-only, typed, -validated, preference, or configuration variables known to the supported -PowerShell runtime. The preference inventory SHALL include documented lazy and -configuration-dependent names even when a fresh `Get-Variable` inventory omits -them. -Scoped/provider binding forms SHALL fail closed. +### Requirement: PowerShell approvals prove authored commands, not ambient resolution +`PwshParserOptions.InitialStateMode` SHALL default to `Unknown` and SHALL remain +source and binary compatible. Neither that default nor an ambient alias, +function, module, profile, executable lookup, or inherited variable SHALL by +itself make a static authored command occurrence incomplete. The parser SHALL +prove that it discovered the executable syntax submitted by the caller; it +SHALL NOT claim to prove the runtime command selected by the host. + +`Unknown` mode SHALL keep a loop-dependent effective value `Unknown` when an +ambient typed, validated, read-only, or constant binding could coerce or reject +the assignment. The surrounding static command occurrence MAY remain complete; +value precision is independent from authored executable discovery. + +`IsolatedNonInteractiveNoProfile` SHALL assert that the complete source runs in +a newly spawned noninteractive PowerShell process with profiles disabled and +without a reused or caller-initialized runspace. It SHALL permit exact or finite +literal values for ordinary unscoped bindings. It SHALL NOT require a pinned +module, alias, function, `PATH`, or executable-resolution baseline. The +supported-name boundary SHALL continue to exclude automatic, constant, +read-only, preference, configuration, scoped, and provider bindings whose +special semantics are visible from the submitted binding name. 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. +share supported authored binding and cwd state. Decoded child hosts SHALL clear +host-dependent value facts that are not independently proved, but SHALL retain +complete static authored command occurrences. Recognized source-level variable, +alias, function, or module mutation SHALL invalidate later affected proofs in +every observing scope; cwd-only mutation SHALL retain independent authored +binding facts. #### Scenario: Computed Invoke-Expression invalidates current-runspace state - **WHEN** isolated-mode PowerShell parses `foreach ($f in 'safe.txt') { }; Invoke-Expression $code; git $f` - **THEN** the computed payload remains an incomplete occurrence -- **THEN** the later `git` occurrence has Unknown working directory and effective `$f` value and is incomplete because the payload can mutate location, variables, aliases, functions, or modules +- **THEN** the later `git` occurrence has Unknown working directory and effective `$f` value and is incomplete because the authored payload can hide commands and mutate location, variables, aliases, functions, or modules - **THEN** the canonical alias, static call-operator spelling, and supported module-qualified spelling have the same effect - **WHEN** a computed `Invoke-Expression` occurs inside a bounded `foreach` region whose transfer cannot be modeled - **THEN** the complete parse fails atomically rather than retaining stale loop state @@ -357,13 +354,13 @@ initial-state assertion. - **THEN** the second command occurrence is incomplete because authored identity `git` is no longer proved - **THEN** this invalidation applies without requiring the command to be inside or after a loop -#### Scenario: Unknown ambient identity preserves leaves and invalidates continuation state +#### Scenario: Ambient identity uncertainty preserves authored completeness - **WHEN** default-mode PowerShell parses `Write-Output victim.txt; Get-Content relative.txt` - **THEN** default ambient-state uncertainty alone does not invent an observed mutation or discard the v0.2 compatibility leaves -- **THEN** both v0.3 authorization occurrences are incomplete because their command identities are not proved -- **THEN** the second occurrence has unknown cwd and path-dependent facts because the first invocation may resolve to arbitrary in-process code +- **THEN** both v0.3 authorization occurrences are complete authored command occurrences +- **THEN** the second occurrence retains parser-owned cwd and path facts because ambient runtime resolution is outside the approval proof - **WHEN** default-mode PowerShell parses `Get-ChildItem | Remove-Item` -- **THEN** the unproved pipeline fails atomically until pipeline state propagation is modeled +- **THEN** both static authored pipeline stages remain visible and complete unless another authored fact is dynamic or unsupported #### Scenario: Imported session proxies invalidate command identity - **WHEN** PowerShell parses `Import-PSSession $session -CommandName git -AllowClobber; git child.txt` @@ -399,19 +396,21 @@ initial-state assertion. - **THEN** quoted call-operator spelling and built-in cmdlets with unapproved verbs cannot bypass the same rule - **THEN** `Microsoft.PowerShell.Utility\Invoke-Expression` remains the one separately modeled module-qualified wrapper -#### Scenario: Unknown ambient PowerShell state withholds a finite proof +#### Scenario: Unknown ambient PowerShell state keeps effective values unknown - **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 +- **THEN** the loop structure and body command remain visible and complete +- **THEN** the body occurrence's effective `$f` value is Unknown +- **THEN** the parser does not mistake authored iterable text for a runtime value when an ambient binding can coerce or reject it #### 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 }` +- **WHEN** the caller selects `IsolatedNonInteractiveNoProfile` for a newly spawned noninteractive no-profile host and parses `foreach ($f in @('a','b')) { Write-Output $f }` - **THEN** the bounded analyzer may publish the finite string domain `a`, `b` +- **THEN** no pinned module or command-resolution baseline is required -#### Scenario: Typed or read-only ambient binding is not erased by syntax +#### Scenario: Typed or read-only ambient binding is an executor externality - **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 +- **THEN** the static body command may remain complete +- **THEN** its loop-dependent effective value is Unknown rather than the authored string text #### Scenario: Built-in preference binding is not an ordinary string slot - **WHEN** isolated-mode PowerShell parses a loop binding named `ConfirmPreference`, `ErrorActionPreference`, or another known built-in preference or configuration variable @@ -420,8 +419,8 @@ initial-state assertion. #### 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 +- **THEN** the child retains complete authored commands and ordinary literal loop values +- **THEN** the child does not inherit exact environment, home, provider, or cwd facts that were not independently proved #### Scenario: Current-runspace evaluation shares state - **WHEN** a supported `$()` or static `Invoke-Expression` region mutates a loop-relevant binding or command-resolution fact @@ -637,7 +636,7 @@ partition merely to publish exact continuation facts. #### 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** the decoded child `Get-Date` remains a complete authored command even though child host 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 @@ -828,7 +827,7 @@ SHALL NOT prove concurrency. #### Scenario: One remote target has an isolated synchronous region - **WHEN** isolated-mode PowerShell parses `Invoke-Command -ComputerName server -ScriptBlock { Get-Item child.txt }; Get-Item host.txt` - **THEN** the region timing is Synchronous and its cardinality is Once -- **THEN** the body working directory and mutable state are Unknown and incomplete +- **THEN** the body command is complete while its working directory and host-dependent state remain Unknown - **THEN** the following host command retains its exact local state #### Scenario: Remote asynchronous switches prove only concurrency @@ -844,7 +843,7 @@ SHALL NOT prove concurrency. - **THEN** it does not prove multiple targets - **WHEN** PowerShell instead parses a runtime `-Session $session` target - **THEN** timing and cardinality are Unknown unless an enabled asynchronous switch independently proves Concurrent timing -- **THEN** every remote body command remains visible and incomplete +- **THEN** every static remote body command remains visible and complete while the target-dependent region facts remain Unknown #### Scenario: Direct invocation origin survives without source text - **WHEN** a consumer receives direct call and dot-source execution-region nodes diff --git a/openspec/changes/v0-3-structured-shell-analysis/specs/executable-command-projection/spec.md b/openspec/changes/v0-3-structured-shell-analysis/specs/executable-command-projection/spec.md index 5429831..ae09da3 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/specs/executable-command-projection/spec.md +++ b/openspec/changes/v0-3-structured-shell-analysis/specs/executable-command-projection/spec.md @@ -139,9 +139,12 @@ SHALL NOT omit the body or authorize it as inert data. - **THEN** `Commands` and `Clauses` are empty ### Requirement: Occurrence completeness is explicit -Each occurrence SHALL state whether its command identity, structural ancestry, -and parser-owned shell analysis are complete. No incomplete occurrence SHALL -be sufficient authorization evidence. +Each occurrence SHALL state whether its authored command identity, structural +ancestry, executable-region discovery, and parser-owned authored shell analysis +are complete. Completeness SHALL NOT claim that ambient aliases, functions, +modules, profiles, executable lookup, or inherited environment select a +particular runtime implementation. No incomplete occurrence SHALL be sufficient +authorization evidence. #### Scenario: Dynamic command identity - **WHEN** PowerShell parses a supported structure whose body invokes `& $exe arg` @@ -158,12 +161,11 @@ be sufficient authorization evidence. - **THEN** the `Write-Output` occurrence may be structurally complete - **THEN** its effective `$item` value remains unknown because pipeline objects are not evaluated -#### Scenario: Unknown PowerShell identity preserves compatibility evidence +#### Scenario: Ambient PowerShell resolution does not erase authored completeness - **WHEN** default-mode PowerShell parses `Write-Output victim.txt` - **THEN** one v0.2 compatibility `Clause` remains visible -- **THEN** the v0.3 occurrence is incomplete because ambient command resolution may shadow the authored name -- **WHEN** the same source is parsed under the constrained isolated-host contract -- **THEN** the occurrence command identity is complete +- **THEN** the v0.3 occurrence is complete for the authored `Write-Output` identity +- **THEN** runtime shadowing remains outside the approval-grammar proof ### Requirement: Source order is deterministic The occurrence collection SHALL be ordered by authored command occurrence, diff --git a/openspec/changes/v0-3-structured-shell-analysis/specs/structured-shell-syntax/spec.md b/openspec/changes/v0-3-structured-shell-analysis/specs/structured-shell-syntax/spec.md index 6fa7907..10cbc5c 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/specs/structured-shell-syntax/spec.md +++ b/openspec/changes/v0-3-structured-shell-analysis/specs/structured-shell-syntax/spec.md @@ -163,7 +163,7 @@ that `SimpleCommandSyntax` and SHALL identify the exact script-block - **THEN** a realistic argument completer is not partially authorized from only its post-declaration body #### Scenario: Known non-executing script-block data stays data -- **WHEN** a constrained canonical-command context parses `Write-Output { Remove-Item target.txt }` +- **WHEN** PowerShell parses the static authored command `Write-Output { Remove-Item target.txt }` - **THEN** the script block remains one opaque compatibility argument - **THEN** no execution region or `Remove-Item` occurrence is invented diff --git a/openspec/changes/v0-3-structured-shell-analysis/tasks.md b/openspec/changes/v0-3-structured-shell-analysis/tasks.md index 2f74683..fbc9ee4 100644 --- a/openspec/changes/v0-3-structured-shell-analysis/tasks.md +++ b/openspec/changes/v0-3-structured-shell-analysis/tasks.md @@ -173,20 +173,31 @@ and the shared structural-depth cap. - [x] 7.2 Emit iterator and loop-body occurrences plus conservative compatibility clauses. - Iterator pipelines and direct `$()` are recursively visible with authored - roles and ancestry. Every loop-body occurrence remains incomplete until - tasks 7.3 and 7.4 prove binding values and runspace state; recognized - 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. + roles and ancestry. The initial structural slice emitted incomplete body + occurrences until tasks 7.3 and 7.4 added binding and runspace analysis. + Alpha.3 still leaves default-mode occurrences incomplete for ambient + resolution; task 7.2c corrects that behavior. Explicit iterator/body state + mutation and dynamic invocation remain strict, and 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. + canonical specs and case-specific design corpus. The ambient-resolution + portion of this completed alpha.3 design is superseded by 7.2b; the public API + remains compatible. +- [x] 7.2b Correct the approval boundary so PowerShell matches Bash's + authored-command model: ambient runtime resolution is outside occurrence + completeness, while explicit source mutations, computed identities, hidden + execution, and unsupported syntax remain strict. Preserve the existing + `PwshInitialStateMode` API shape. +- [ ] 7.2c Implement authored-command completeness for default-mode static + PowerShell commands, pipelines, decoded children, and known script-block + receivers without weakening explicit mutation or dynamic-execution checks. - [x] 7.3 Derive exact and finite string domains without treating pipeline objects as literal strings. - The PowerShell-specific value pass consumes lexer provenance, composes case-insensitive distinct active bindings, publishes bounded literal - scalar/array domains only under the explicit isolated-runspace contract, + scalar/array domains under the alpha.3 isolated-runspace contract, and collapses object, null, unsupported, and over-cap values to Unknown. The internal plan retains ordered duplicate visits and an exact authored count separately from its public set summary; unknown object iterables are @@ -194,7 +205,9 @@ atomically; a pinned documented preference inventory covers lazy names and a live PowerShell 7.x oracle guards the fresh-host inventory. Decoded child hosts, current-runspace wrappers, redirect values, same-name nested - overwrites, and post-loop state remain conservative for tasks 7.4-7.6. + overwrites, and post-loop state remain conservative for tasks 7.4-7.6. The + authored-command correction leaves this effective-value contract intact; + isolated mode no longer implies a pinned command-resolution baseline. - [x] 7.4 Propagate PowerShell scope and location state according to the locked statement semantics. - The PowerShell-specific abstract-state pass now owns case-insensitive persistent bindings, ordered/empty/zero-or-more execution, occurrence joins, @@ -236,14 +249,14 @@ - Supported non-pipeline bodies remain visible and incomplete. An interior pipeline whose stage identity is unproved fails the whole parse atomically with empty authorization projections. - - 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`. + - Alpha.3 kept canonical, alias, and supported module-qualified + `Write-Output` receivers opaque only under constrained state. Task 7.2c + supersedes the ambient-state part: static authored receivers stay data in + default mode, while a matching observed source-level mutation still + downgrades to an unknown incomplete region. Executable-corpus entries pin + proved data, an unknown receiver, proved local `Invoke-Command`, the exact + module-qualified-looking mutation 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.