Implement Bash loop effective cwd transfers

IMPLEMENTATION_PLAN.md

@@ -283,35 +283,21 @@ priorities.
       leaves preserve authored dynamic operands. Loop binding and cwd
       mutation fail closed, loops reached after recognized prior shell-state
       mutation fail closed, and occurrence cwd remains Unknown.
-- [ ] Design and implement structure-aware Bash abstract-state analysis before
-      enabling cwd-changing loop bodies or claiming the complete `for ... in`
-      vertical slice. The parse-order attribution model cannot soundly publish
-      occurrence cwd across pipelines, conditional lists, substitutions, and
-      repeated iterations. The design now requires internal success/failure
-      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. 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`
-      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 across these two analyzer slices.
+- [x] Design and implement structure-aware Bash abstract-state analysis for the
+      complete bounded `for ... in` state slice. The analyzer owns
+      success/failure partitions, failure-aware cwd transfer, conservative
+      pipeline state, ordered duplicate-preserving loop plans, persistent loop
+      bindings, empty iteration, occurrence-fact joins, substitution isolation,
+      and explicit decoded-wrapper remapping. Unknown-cardinality loops use
+      bounded fixed-point widening, a 4096-transition global budget fails nested
+      cross-products atomically, and complete effective argv is re-evaluated for
+      every visit. Loop-derived `cd` options, terminators, invalid/multiple
+      operands, recursive exact `command` / `builtin` dispatch, physical-path
+      compatibility sanitation, and post-loop binding mutation are pinned by
+      unit tests, native Bash oracles, the design corpus, and executable corpus.
+      All unmodeled mutations, dynamic dispatch, and control transfers remain
+      fail closed. Next add the Netclaw approval matrix before calling the Bash
+      consumer integration complete.
 - [ ] 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,

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

@@ -526,6 +526,19 @@ 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.
 
+Static dispatch is interpreted from the same ordered element stream. Exact
+`command -p`, `command --`, and `builtin --` wrappers may recurse to `cd` or
+`chdir`; `command -v` / `-V` is a nonmutating query. Invalid or dynamic wrapper
+grammar does not dispatch. If a rebound physical option changes which authored
+element is the operand, every compatibility resolution made unsafe by that
+visit is cleared by element coordinate in both `Clause.Args` and
+`Clause.Elements`. The first operand ends option recognition; every later word
+is a second operand and therefore an exact failure. Unknown quoted one-word
+values may conservatively produce unknown cwd on success, but unquoted field
+splitting or globbing of a tracked loop binding leaves argv cardinality
+unproved and fails the region atomically. Ambient dynamic values retain the
+older compatibility contract's conservative unknown-state behavior.
+
 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

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

@@ -319,7 +319,18 @@ argument's complete shell-value provenance for each concrete visit. Effective
 argument facts at one authored occurrence SHALL join across reachable visits.
 State transfers such as `cd` SHALL parse the complete effective argv, including
 candidate-derived options and option terminators, rather than substituting only
-an operand. A transfer such as `break`, `continue`, `return`, `exit`, or `exec`,
+an operand. Exact `command` options `-p` and `--` and the exact `builtin --`
+delimiter SHALL be recursively unwrapped; `command -v` / `-V` SHALL remain a
+nonmutating query, while invalid or dynamic wrapper grammar SHALL fail closed.
+When effective option grammar makes an authored path resolution unsafe, the
+compatibility `Arg` and corresponding `ClauseElement` resolutions SHALL both be
+cleared without rewriting their authored spelling or flag classification.
+Option recognition SHALL stop at the first operand. An exact invalid option or
+second operand SHALL have no success partition, and a tracked loop-binding
+expansion whose argv cardinality is not proved SHALL make the containing region
+unparseable. Ambient dynamic values retain the compatibility contract's
+conservative unknown-state behavior. A
+transfer such as `break`, `continue`, `return`, `exit`, or `exec`,
 including recursively wrapped builtin forms, SHALL make the containing region
 unparseable until the analyzer implements that transfer explicitly. `eval`,
 `source` / `.`, execution-bearing `trap`, and mutation of tracked bindings
@@ -388,6 +399,23 @@ partition merely to publish exact continuation facts.
 - **THEN** the second visit treats `/tmp` as the operand under the resulting option grammar
 - **THEN** no state transfer reuses the authored `$f` flag classification
 
+#### Scenario: Loop-derived physical option sanitizes compatibility paths
+- **WHEN** isolated-mode Bash analyzes `for f in -P; do cd "$f" ./sub && cat file.txt; done`
+- **THEN** the effective argv is `cd -P ./sub`
+- **THEN** both compatibility projections clear the authored `/work/sub` resolution
+- **THEN** the reached `cat` has unknown cwd and no exact relative-path resolution
+- **WHEN** the loop candidate is `--` instead
+- **THEN** `./sub` remains the exact logical operand and the reached path resolves under `/work/sub`
+
+#### Scenario: Exact dispatch wrappers preserve cwd transfer grammar
+- **WHEN** a loop body invokes `command -p -- builtin -- cd "$f"`
+- **THEN** the analyzer recursively proves the wrapper grammar
+- **THEN** it interprets only the words after `cd` as the effective transfer argv
+- **WHEN** `command -v` or `command -V` is used
+- **THEN** the wrapper is a query and does not mutate cwd
+- **WHEN** a wrapper option is invalid or dynamic
+- **THEN** the loop remains fail closed
+
 #### Scenario: Empty-loop failure continuation is unreachable
 - **WHEN** isolated-mode Bash parses `for f in; do false; done || cat relative.txt`
 - **THEN** the empty loop has only a reachable success exit

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

@@ -95,15 +95,16 @@
       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
+    - [x] 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.
+    when no modeled transfer can disagree. Complete effective `cd` argv,
+    recursive exact `command` / `builtin` dispatch, failure-only invalid forms,
+    physical-path sanitation, and persistent post-loop binding protection are
+    implemented. It still rejects every unmodeled shell-state mutation,
+    control transfer, nested active-binding reuse, and dynamic dispatch.
 - [ ] 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.