Implement analyzer-owned Bash loop state

IMPLEMENTATION_PLAN.md

@@ -291,11 +291,15 @@ priorities.
       flow partitions, failure-aware `cd`, conservative `lastpipe` / `pipefail`,
       ordered duplicate-preserving loop plans, inherited but isolated
       decoded-wrapper state, and dynamic fail-closed compatibility attribution
-      whenever cwd joins to Unknown. Keep OpenSpec task 6.5 open, then add the
-      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. An adversarial
+      whenever cwd joins to Unknown. The analyzer now owns persistent loop
+      bindings, ordered and empty iteration, occurrence-fact joins, unreachable
+      flow partitions, substitution inheritance, and explicit decoded-wrapper
+      remapping of loop plans and argument provenance. Unknown-cardinality
+      loops use bounded fixed-point widening, and a 4096-transition global
+      budget fails nested cross-products atomically. Static bodies retain an
+      exact incoming cwd when no transfer can change it. Keep OpenSpec task 6.5
+      open for full effective-argv transfer and removal of the temporary loop
+      mutation rejection, then add the Netclaw approval matrix. 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`
@@ -307,7 +311,7 @@ priorities.
       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.
+      pipelines across these two analyzer slices.
 - [ ] 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

@@ -599,7 +599,9 @@ 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.
+an artificial cross-product. The analyzer permits at most 4096 total loop-body
+transitions per parse; exceeding that resource budget makes the complete result
+unparseable rather than returning a partial cross-product.
 
 Each concrete iteration assigns its candidate into the analyzer variable map,
 re-evaluates the complete effective argument vector for every body occurrence,

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

@@ -453,10 +453,11 @@ proved syntax tree, not by exposing the compatibility parser's mutable
 parse-order cwd attribution. Parse order is not execution-state order for
 pipelines or conditional lists, and one symbolic loop-body parse cannot prove
 the cwd of later iterations. The compatibility attribution path remains a
-v0.2 leaf-construction detail. Until the abstract pass lands, loop cwd mutation
-fails closed, recognized shell-state mutation before or inside a loop fails
-closed, nested reuse of an active Bash binding name fails closed, and
-occurrence `WorkingDirectory` stays `Unknown`.
+v0.2 leaf-construction detail. The ordered-binding pass may retain exact cwd
+for reached nonmutating loop occurrences. Loop cwd mutation, recognized shell-
+state mutation before or inside a loop, and nested active-name reuse continue
+to fail closed until complete effective-argv transfers and repeated mutable
+state are modeled.
 
 Bash command substitution executes in an isolated subshell state. State changes
 affect later commands inside that substitution but never the containing command
@@ -492,6 +493,11 @@ wrapped builtin forms such as `builtin break` and `command exit`. `eval`,
 `source` / `.`, and execution-bearing `trap` also fail the whole region closed
 unless every executable region and state transfer is discovered.
 
+The analyzer also has a parse-wide budget of 4096 loop-body transitions.
+Concrete nested products and fixed-point visits consume the same budget; an
+overflow fails the complete parse atomically so an adversarial input cannot
+force an unbounded cross-product or receive a partial security projection.
+
 The internal loop plan is distinct from the public value-domain summary. It
 retains an executable word plan parameterized by the incoming analyzer binding
 map, plus a cardinality of `Never`, `OneOrMore`, or `ZeroOrMore`. Evaluating the

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

@@ -362,6 +362,11 @@ partition merely to publish exact continuation facts.
 - **THEN** the internal iteration cardinality is `Never`
 - **THEN** the following `pwd` retains the exact incoming cwd
 
+#### Scenario: Reached nonmutating loop body retains incoming cwd
+- **WHEN** isolated-mode Bash parses a supported loop whose body cannot change cwd
+- **THEN** each reached body occurrence retains the exact incoming cwd
+- **THEN** a structurally present but unreachable body or continuation still receives conservative cwd facts
+
 #### Scenario: Duplicate iteration values retain order
 - **WHEN** isolated-mode Bash parses `for f in a b a; do :; done; printf '%s' "$f"`
 - **THEN** the internal iteration plan retains `a`, `b`, `a` in that order
@@ -372,6 +377,11 @@ partition merely to publish exact continuation facts.
 - **THEN** the internal plan exceeds the concrete-iteration cap
 - **THEN** it uses bounded fixed-point analysis instead of treating one distinct public value as one visit
 
+#### Scenario: Nested loop analysis stays resource bounded
+- **WHEN** nested concrete loops require more than 4096 total body transitions
+- **THEN** the complete parse is unparseable
+- **THEN** no partial occurrence or compatibility projection is published
+
 #### Scenario: Loop-derived cd option is rebound from effective argv
 - **WHEN** isolated-mode Bash analyzes `for f in -P /tmp; do cd "$f"; done`
 - **THEN** the first visit treats `-P` as a `cd` option rather than a path operand

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

@@ -87,17 +87,23 @@
       make the analyzer own persistent bindings, parameterized ordered plans,
       full argument provenance/effective-argv transfer, occurrence-fact joins,
       and unreachable exit partitions.
-    - [ ] 6.5c.2 Implement that corrected contract and corpus-pin `HOME`,
-      `RANDOM`, `LINENO`, `PATH`, `CDPATH`, `IFS`, 32/33 ordered visits,
-      zero-iteration state, loop-derived `cd` options, nested correlation,
-      wrapped transfers, wrapper mapping, substitutions, and pipelines.
-  - The first static-value slice deliberately leaves occurrence cwd Unknown
-    and rejects loop shell-state mutation, nested active-binding reuse, or
-    loops reached after recognized prior shell-state mutation. A separate
-    structure-aware abstract-state pass is required
-    before enabling cwd-changing bodies;
-    mutable parse-order attribution is unsound across pipelines, `&&` / `||`,
-    substitutions, and repeated iterations.
+    - [x] 6.5c.2 Make the analyzer own persistent bindings, ordered and empty
+      iteration, visit-joined effective arguments, unreachable exit partitions,
+      substitution inheritance, and explicit decoded-wrapper remapping. Pin
+      special-name rejection, 32/33 visit boundaries, duplicate order,
+      zero-iteration state, nested correlation, substitutions, pipelines, and
+      wrapper provenance in unit tests and the Bash corpus. Use bounded
+      fixed-point widening for unknown cardinality and fail atomically after
+      4096 total loop-body transitions.
+    - [ ] 6.5c.3 Re-parse each visit's complete effective argv for state
+      transfers, including loop-derived `cd` options and wrapped dispatch;
+      carry those transfers through the bounded fixed point, then remove only
+      the temporary mutation rejections whose transfers are fully modeled.
+  - The analyzer now publishes exact incoming cwd for reached loop occurrences
+    when no modeled transfer can disagree. It still rejects loop shell-state
+    mutation, nested active-binding reuse, and loops reached after recognized
+    prior shell-state mutation until 6.5c.3 reclassifies complete effective argv
+    and models the corresponding repeated transfers.
 - [ ] 6.6 Cover empty iterables, separators, multiline bodies, redirects, pipelines, nested loops, and wrapper boundaries.
 - [ ] 6.7 Add adversarial cases for option injection, mutation, unquoted expansion, indirect expansion, substitutions, and cap overflow.
 - [ ] 6.8 Add sanitized Bash corpus entries and Netclaw allow/prompt/deny integration cases.