Require explicit Bash loop initial state

IMPLEMENTATION_PLAN.md

@@ -295,7 +295,19 @@ priorities.
       remaining loop cases and Netclaw approval matrix after implementation.
       The non-loop state engine is now implemented for lists, pipelines,
       substitutions, subshells, and decoded wrappers; loop iteration state and
-      removal of the temporary mutation rejection remain next.
+      removal of the temporary mutation rejection remain next. An adversarial
+      pre-implementation review halted the first loop-state draft: parser-time
+      binding frames could not model zero-iteration persistence, correlated
+      nested iterables, special Bash variables, or candidate-derived `cd`
+      options. The corrected contract now requires an explicit
+      `BashInitialStateMode`, a conservative supported scalar-name boundary,
+      analyzer-owned persistent bindings, parameterized ordered plans, complete
+      argument provenance/effective-argv transfer, occurrence-fact joins, and
+      unreachable flow partitions. Implement that contract before enabling any
+      cwd-changing loop body. Corpus-pin `HOME`, `RANDOM`, `LINENO`, `PATH`,
+      `CDPATH`, `IFS`, 32/33 ordered visits, zero iterations, nested
+      correlation, wrapped transfers, wrapper mapping, substitutions, and
+      pipelines in the same vertical slice.
 - [ ] Complete PowerShell `$()` discovery in `foreach` expressions and add the
       Netclaw approval-matrix cases. The simple-command slice is delivered for
       ordinary, adjacent, quoted, here-string, redirect, standalone,

SPEC.md

@@ -107,10 +107,20 @@ public sealed class PwshParser : IShellParser
 /// (added v0.2.0). HomeDirectory / WorkingDirectory live here.</summary>
 public abstract record ShellParserOptions { ... }
 
+/// <summary>Declares which ambient Bash variable facts the caller can prove.</summary>
+public enum BashInitialStateMode
+{
+    Unknown,
+    IsolatedNonInteractive,
+}
+
 /// <summary>Configuration knobs for BashParser. As of v0.2.0 a sealed
 /// record deriving from ShellParserOptions; the v0.1 object-initializer
 /// shape is unchanged.</summary>
-public sealed record BashParserOptions : ShellParserOptions;
+public sealed record BashParserOptions : ShellParserOptions
+{
+    public BashInitialStateMode InitialStateMode { get; init; }
+}
 
 /// <summary>Configuration knobs for PwshParser (v0.2.0). Empty — the
 /// resolver knobs live on ShellParserOptions.</summary>
@@ -230,6 +240,36 @@ public sealed record ParsedCommand
 }
 ```
 
+`BashInitialStateMode.Unknown` is the default. In this mode the parser does
+not publish bounded loop-variable facts: an ambient shell may already have
+made the binding readonly, integer-valued, a nameref, exported, or otherwise
+semantically significant. A Bash loop whose safety depends on such a binding
+is therefore unparseable rather than being analyzed as an ordinary scalar.
+
+`BashInitialStateMode.IsolatedNonInteractive` is an explicit caller assertion,
+not a parser discovery. It means the complete source is executed by a newly
+spawned non-interactive Bash process, no profile or `BASH_ENV` / `ENV` startup
+content is loaded, and no inherited environment entry carries the loop-bound
+name. A consumer may select this mode only when its execution path enforces
+those conditions. Supplying this option while executing in a reused,
+interactive, startup-scripted, or uncontrolled environment invalidates the
+analysis.
+
+Recognized variable-state mutation in the analyzed source invalidates isolated
+mode for every later region that can observe it. In particular, a decoded
+`bash -c` child after `export` is analyzed with unknown initial variable state;
+the option is not blindly copied into the child. Cwd-only state changes retain
+the caller's initial-variable assertion.
+
+Even in isolated mode, the v0.3 bounded loop grammar accepts only ordinary
+lowercase scalar binding names matching `[a-z][a-z0-9_]*`, excluding
+`auto_resume` and `histchars`. `_`, uppercase names, and every name outside
+that boundary fail the complete loop region closed. This deliberately excludes
+Bash magic variables and resolver- or executable-identity-sensitive names such
+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.
+
 For a successful result, every authored simple command appears once in
 `Syntax`, once in `Commands`, and once in `Clauses`, with all three projections
 referencing the identical in-memory `Clause` instance. Serialization is not
@@ -534,6 +574,76 @@ simple-command leaves do not independently increment it. Exceeding 16
 structural containers or 5 decoded-command wrapper recursions makes the entire
 result unparseable.
 
+#### Bash bounded loop state
+
+Loop bindings are analyzer-owned shell state; they are not lexical parser
+frames. A nonempty Bash loop leaves its final assigned value visible after
+`done`, a loop that executes zero times preserves the incoming value, and a
+same-name nested loop does not restore an outer value. v0.3 may continue to
+reject nested active-name reuse until that overwrite behavior is implemented;
+it must never model the construct as lexical shadowing.
+
+The Bash front end retains every iterable word and every resolver-relevant
+argument fragment as parser-owned internal provenance. The abstract-state pass
+then evaluates the iterable once from its incoming variable state and creates
+one of these internal plans:
+
+- `Never` for an explicit empty iterable;
+- an ordered, duplicate-preserving sequence for at most 32 concrete
+  iterations; or
+- `ZeroOrMore` / `OneOrMore` fixed-point analysis when cardinality or an
+  ordered sequence is not bounded.
+
+The public `FiniteSet` is only a value summary. It is never used as an
+iteration plan: `a b a` performs three state transitions and leaves an exact
+final binding of `a`; 33 authored values use widening even when every value is
+the same. An iterable that depends on an outer binding is evaluated separately
+for each concrete outer visit so correlated nested state is not flattened into
+an artificial cross-product.
+
+Each concrete iteration assigns its candidate into the analyzer variable map,
+re-evaluates the complete effective argument vector for every body occurrence,
+and carries the joined reachable cwd and variable state into the next
+iteration. This re-evaluation includes state-transfer option grammar. For
+example, a loop-derived `cd` argument may become `-P`, `--`, `-`, or an
+operand; the analyzer may not substitute only an operand string while retaining
+authored flag classification. Effective argument facts at one authored
+occurrence join the values from every reachable visit.
+
+Bash flow retains separate reachable success and failure states. `&&` analyzes
+only a reachable success continuation, `||` only a reachable failure
+continuation, and sequence operators consume their join. A missing partition
+is unreachable and must not be replaced with the joined input merely to
+populate exact facts. Structurally present but unreachable commands remain in
+the syntax/occurrence projection with conservative facts. An empty loop exits
+successfully without a body transition; a known nonempty loop exposes the
+final body's exit status; a zero-or-more loop joins its zero path with every
+reachable normal exit. Bounded fixed-point analysis widens differing cwd or
+variable values to `Unknown` rather than selecting one path.
+
+`cd` and `chdir` use the effective argument vector for the current visit.
+`pushd` and `popd` may be recognized only with unknown success cwd until the
+directory stack is modeled. Variable mutators (`read`, `unset`, `printf -v`,
+`export`, `declare`, and equivalents), `eval`, `source` / `.`, and
+execution-bearing `trap` make the complete loop region unparseable. The same is
+true for `break`, `continue`, `return`, `exit`, and `exec` until their transfers
+are implemented. Recognition recursively unwraps statically proved `command`
+and `builtin` dispatch; a wrapper must not bypass the rejection.
+
+Substitutions and subshells inherit the current variable/cwd state but discard
+their state changes on exit. Decoded Bash command wrappers inherit invocation
+cwd but no loop binding unless export is separately proved. Pipeline stages
+enter from the same pipeline input; possible `lastpipe` leakage joins the full
+cwd and variable state, independently of conservative `pipefail` exit
+partitioning.
+
+Compatibility arguments always retain authored loop-variable spelling. A
+variable-derived path that is not independently exact keeps or becomes
+`DynamicSkip`, and a relative path whose reachable visit cwds disagree loses
+its static resolution. In particular, compatibility projection may not retain
+the configured `$HOME` resolution after a loop binds `HOME`, even though that
+binding is outside the v0.3 supported-name boundary.
+
 ### Explicit redirect analysis (v0.3)
 
 Occurrence-specific redirect analysis is additive. The existing `Redirect`
@@ -1035,12 +1145,17 @@ bash_else            := "else" bash_script(stop = "fi")
 
 list_sep             := ";" | NEWLINE
 list_terminator      := ";" | NEWLINE+
-binding_name         := shell_identifier
+binding_name         := supported_scalar_binding
+supported_scalar_binding := [a-z][a-z0-9_]*
+                            except "auto_resume" and "histchars"
 iterable_word        := word | quoted_string | supported_substitution
 ```
 
 The supported stable-v0.3 set is the existing simple-command grammar plus
-`for name in words`, `while` / `until`, and `if` / `elif` / `else`. Every fully
+`for name in words`, `while` / `until`, and `if` / `elif` / `else`. Bash
+accepts additional shell identifiers as loop variables, but this bounded
+grammar fails them closed for the initial-state reasons specified in §2.
+Every fully
 delimited `$()` command substitution in a supported simple-command argument,
 redirect value, iterable, or expanding heredoc body is recursively parsed and
 exposes its inner commands; its produced value remains `Unknown`. A nested

docs/CONSUMER_GUIDE.md

@@ -169,6 +169,35 @@ are:
    scope, cwd, or redirects. A structurally complete occurrence may still have
    an unknown value; those are separate facts.
 
+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
+readonly, integer-valued, a nameref, exported, or shell-owned. Select
+`IsolatedNonInteractive` only when the same component that calls the parser
+also enforces all of these execution conditions:
+
+- the source is the complete input to a newly spawned non-interactive Bash;
+- no profile, `BASH_ENV`, or `ENV` startup content can run; and
+- no inherited environment entry carries a loop-bound name.
+
+```csharp
+var parser = new BashParser(new BashParserOptions
+{
+    WorkingDirectory = workingDirectory,
+    InitialStateMode = BashInitialStateMode.IsolatedNonInteractive,
+});
+```
+
+Do not select the mode merely because a command *looks* self-contained. A
+consumer that parses under isolated assumptions but executes in a reused or
+startup-scripted shell has invalidated the authorization proof. Stable v0.3
+also fails uppercase, underscore-prefixed, and Bash-owned lowercase loop names
+closed; `HOME`, `RANDOM`, `LINENO`, `PATH`, `CDPATH`, and `IFS` are intentionally
+outside the first bounded scalar grammar. The parser also downgrades a decoded
+`bash -c` child's initial state after a preceding variable mutation such as
+`export`; resolver-only option cloning for an exact cwd retains the independent
+variable-state assertion.
+
 Heredoc and Bash here-string bodies are stdin data, not implicit child commands
 or filesystem paths. Authorize any command substitutions surfaced from an
 expanding heredoc as normal occurrences, then let executable-specific policy

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

@@ -406,6 +406,23 @@ shell rules prove the resulting argument boundary. Unquoted Bash expansion,
 PowerShell object-valued pipelines, indirect expansion, mutation, and
 cross-product explosion remain unknown until separately specified.
 
+Bash loop binding also requires a proved initial shell-variable environment.
+`BashParserOptions.InitialStateMode` defaults to `Unknown`; bounded Bash loop
+analysis is unavailable in that mode because an ambient binding may be
+readonly, integer-valued, a nameref, exported, or otherwise stateful.
+`IsolatedNonInteractive` is a caller assertion that the complete source runs in
+a new non-interactive Bash process without profile, `BASH_ENV`, or `ENV`
+startup content and without an inherited entry for the bound name. The v0.3
+positive grammar is deliberately limited to lowercase ordinary scalar names
+matching `[a-z][a-z0-9_]*`, excluding `auto_resume` and `histchars`. Names
+outside that boundary fail the whole loop region closed. This excludes Bash
+magic and identity-sensitive bindings including `RANDOM`, `LINENO`, `HOME`,
+`PATH`, `CDPATH`, and `IFS` without attempting an incomplete denylist.
+Recognized source-level variable mutation invalidates isolated mode in every
+later scope that can observe it. A decoded `bash -c` after `export` therefore
+enters with `Unknown` initial variable state, while a cwd-only transfer retains
+the caller's variable-state assertion.
+
 Effective values are shell facts, not executable semantics. The analysis must
 preserve both the authored shell classification and each proved effective
 value. PowerShell does not retroactively turn a string value such as `-Force`
@@ -457,6 +474,11 @@ visible to later inner occurrences but do not leak on wrapper exit. This v0.3
 occurrence rule corrects the old compatibility attribution shortcut without
 requiring v0.2 leaves to invent a new exact path.
 
+Decoded-wrapper cloning must remap every parser-owned loop plan and argument
+provenance fact to the cloned syntax/Clause references. Losing a side-table
+entry is not permission to analyze one representative iteration; the wrapper
+region fails closed if the mapping cannot be proved complete.
+
 Exact and finite Bash `for ... in` domains are analyzed in authored iteration
 order within the 32-candidate cap. Each iteration consumes the joined reachable
 state from the preceding iteration, and the loop exit joins every reachable
@@ -471,13 +493,38 @@ wrapped builtin forms such as `builtin break` and `command exit`. `eval`,
 unless every executable region and state transfer is discovered.
 
 The internal loop plan is distinct from the public value-domain summary. It
-retains ordered per-word candidates including duplicates and a cardinality of
-`Never`, `OneOrMore`, or `ZeroOrMore`. Thus `a b a` has a final exact binding of
-`a`, while an explicit empty iterable has no body transition at all. All
-reachable visits to one authored body occurrence join their input facts. If an
-ordered iteration sequence exceeds the candidate budget, the analyzer uses a
-bounded fixed point and widening; it does not select the last retained distinct
-candidate as the post-loop binding.
+retains an executable word plan parameterized by the incoming analyzer binding
+map, plus a cardinality of `Never`, `OneOrMore`, or `ZeroOrMore`. Evaluating the
+plan preserves every concrete candidate in authored order, including
+duplicates. Thus `a b a` has a final exact binding of `a`, while an explicit
+empty iterable has no body transition and preserves the incoming binding. All
+reachable visits to one authored body occurrence join their input facts. The
+32-candidate cap applies to ordered iterations, not distinct public values: 33
+authored `a` words use a bounded fixed point and widening rather than selecting
+one retained value. An inner iterable is re-evaluated for each concrete outer
+binding so nested correlation is not flattened before execution-state
+analysis.
+
+The analyzer, not the structural parser, owns the variable map and binding
+lifetime. Bash loop assignment is not lexical scope: a nonempty loop leaves the
+last value after `done`, zero iterations preserve the incoming value, and a
+same-name inner loop overwrites rather than restoring the outer value. The
+first v0.3 pass may keep active same-name nesting unparseable, but it cannot use
+push/pop shadowing or unconditional parser-time persistence.
+
+Parser-owned side facts retain each argument's complete `ShellValue` fragment
+sequence. For every concrete visit, the analyzer re-evaluates all arguments
+from the current binding map, accumulates effective domains by authored element
+coordinate, and applies state-transfer grammar to the effective argv. This is
+required for `cd "$f"`: a candidate may be `-P`, `--`, `-`, or an operand even
+though the authored expansion was not lexed as an option. Operand-only string
+substitution is not an acceptable shortcut.
+
+An unreachable success or failure partition stays unreachable. `&&` and `||`
+must not replace a missing input partition with `JoinedState` to manufacture
+facts for a structurally present but unreachable continuation. Such commands
+remain projected with conservative facts. This is required before the analyzer
+can expose the one-sided success result of an explicit empty loop.
 
 Bash pipeline stages enter from the same pipeline input state. Ordinary stage
 state does not leak, but the analyzer cannot assume the last stage is isolated