Correct Bash abstract-state semantics

IMPLEMENTATION_PLAN.md

@@ -287,8 +287,12 @@ priorities.
       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. Keep OpenSpec task 6.5 open, then add the remaining
-      loop cases and Netclaw approval matrix after that design is reviewed.
+      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. Keep OpenSpec task 6.5 open, then add the
+      remaining loop cases and Netclaw approval matrix after implementation.
 - [ ] 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

@@ -422,6 +422,15 @@ scope-isolated groups do not leak state. Branches join their possible exit
 states; loops include the zero-iteration path unless shell semantics prove at
 least one iteration.
 
+For Bash, one internal flow result carries separate reachable success and
+failure states. A simple command records its occurrence facts from the joined
+input, then applies shell-specific state transfer to each exit partition.
+`&&` consumes only success, `||` consumes only failure, and `;` / newline
+consume their join. This distinction remains internal: the public cwd domain
+stays `Exact` or `Unknown`. In particular, literal `cd /x` produces `/x` only
+on its success exit and retains the incoming cwd on failure; `cd /x; next`
+therefore cannot make `next` exact unless both possibilities agree.
+
 Implementation must run this as a structure-aware abstract-state pass over the
 proved syntax tree, not by exposing the compatibility parser's mutable
 parse-order cwd attribution. Parse order is not execution-state order for
@@ -440,11 +449,61 @@ subexpression, then the containing command and outer continuation. An unknown
 PowerShell location mutation therefore makes those later working-directory
 facts unknown; the analyzer never falls back to the pre-subexpression cwd.
 
+A decoded `bash -c` / `sh -c` wrapper enters with the abstract cwd of the
+invocation occurrence. It does not inherit unexported loop bindings; exported
+variable state is used only when the analyzer can prove the corresponding
+export semantics, and is otherwise unknown. Inner sequential changes are
+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.
+
+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
+normal exit with the zero-iteration path when zero iterations remain possible.
+Pattern and unknown domains use a bounded fixed point with widening to
+`Unknown`; they are never treated as one representative iteration. Until
+`break`, `continue`, `return`, `exit`, and `exec` have explicit transfer
+semantics, a supported loop region containing one of them fails closed instead
+of publishing incomplete continuation facts. Recognition includes statically
+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 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.
+
+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
+because `lastpipe` is shell-option and job-control dependent. If the last stage
+can mutate supported parent state and execution options are not proved, the
+pipeline exit joins the isolated and current-scope possibilities; disagreement
+becomes `Unknown`. `pipefail` is modeled independently because it can change
+whether a leaked state belongs to the success or failure exit partition. When
+either option is unproved, both partitions conservatively include every
+option-dependent reachable outcome.
+
 The first implementation may collapse any differing cwd states to `Unknown`
 rather than publish a finite cwd set. Selecting one branch's directory is
 never allowed. A later additive version may expose bounded cwd alternatives if
 the consumer contract demonstrates a need.
 
+Compatibility leaves are produced after analysis. If a relative `Arg` or
+`ClauseElement` depended on a cwd that is not exact at that occurrence, its raw
+spelling, path relevance, and source coordinates remain, but `Resolved` is
+cleared. Any false exact synthetic cwd-attribution argument is replaced by the
+existing `Raw="<dynamic-cwd>"`, `Kind=DynamicSkip`, `Resolved=null`,
+`IsCwdAttribution=true` marker. The projection never omits that fail-closed
+signal merely because no exact cwd can be published. This is a security
+correction allowed by the compatibility contract, not an invitation to rewrite
+authored operands with analyzed loop values.
+
 ### Model redirect operation and target independently
 
 The new redirect facts separate:
@@ -572,8 +631,9 @@ into the release specifications before production types are added.
    identical `Clause` instance. This is an in-memory parser-result guarantee,
    not a serialization reference-preservation guarantee.
 4. The initial `Pattern` domain is limited to a Bash path-shaped glob with no
-   dynamic root, substitution, indirect expansion, or unresolved parent
-   traversal. Its `CoveringDirectory` is the exact static directory prefix,
+   dynamic root, substitution, indirect expansion, parent-traversal segment,
+   or glob-bearing dot-prefixed segment that can match `..` when
+   `globskipdots` is disabled. Its `CoveringDirectory` is the exact static directory prefix,
    resolved against an exact cwd when relative. The parser never enumerates the
    filesystem. Bash unmatched-glob settings can change whether the loop has
    zero iterations or yields the literal pattern, but neither outcome escapes
@@ -1308,6 +1368,22 @@ internal sealed record BashForInNode(
     BashBlockNode Body,
     SourceRange Range) : BashNode(Range);
 
+internal readonly record struct BashFlowResult(
+    BashAbstractState? OnSuccess,
+    BashAbstractState? OnFailure);
+
+internal enum BashIterationCardinality
+{
+    Never,
+    OneOrMore,
+    ZeroOrMore,
+}
+
+internal sealed record BashIterationPlan(
+    IReadOnlyList<ShellValueDomain> OrderedWordCandidates,
+    BashIterationCardinality Cardinality,
+    bool RequiresFixedPoint);
+
 internal abstract record PwshNode(SourceRange Range);
 internal sealed record PwshForEachNode(
     PwshBinding Binding,
@@ -1316,6 +1392,12 @@ internal sealed record PwshForEachNode(
     SourceRange Range) : PwshNode(Range);
 ```
 
+Analysis metadata remains attached to the internal authored nodes until the
+syntax, occurrence, and compatibility projections are produced together. An
+implementation may instead use ordered side tables aligned by occurrence
+index, but SHALL NOT key record-valued public nodes with default value equality:
+two textually identical authored commands are still distinct occurrences.
+
 The proposed data flow is:
 
 ```text

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

@@ -255,6 +255,12 @@ Working-directory and supported variable state SHALL be propagated through
 sequential regions and joined across branches and loop exits. Disagreement
 SHALL never be resolved by arbitrarily choosing one path.
 
+The Bash analyzer SHALL internally partition reachable exit state by command
+success and failure. `&&` SHALL continue from the success partition, `||`
+SHALL continue from the failure partition, and `;` or a newline SHALL continue
+from their conservative join. Unreachable partitions are internal analysis
+facts and SHALL NOT require a public API addition.
+
 Bash command substitution SHALL isolate its working-directory and variable
 state from the containing command while retaining sequential state inside the
 substitution. PowerShell `$()` SHALL evaluate in the current runspace scope;
@@ -263,6 +269,19 @@ subexpression, the containing command, and the following outer continuation.
 An unknown mutation SHALL propagate as unknown wherever that shell's scope
 rules make it observable.
 
+Exact and finite Bash `for ... in` domains SHALL be analyzed in authored
+iteration order, including duplicates, within the candidate cap. The analyzer
+SHALL retain independent internal cardinality of `Never`, `OneOrMore`, or
+`ZeroOrMore`; the public finite-set summary SHALL NOT be used as an ordered
+iteration plan. Pattern, unknown, and over-budget domains SHALL use a bounded
+conservative fixed point and SHALL NOT be represented by one arbitrarily
+selected iteration. Every reachable visit to one authored occurrence SHALL
+join its input facts. A transfer such as `break`, `continue`, `return`, `exit`,
+or `exec`, including statically wrapped builtin forms, SHALL make the containing
+region unparseable until the analyzer implements that transfer explicitly.
+`eval`, `source` / `.`, and execution-bearing `trap` SHALL likewise fail closed
+unless all executable regions and transfers are discovered.
+
 #### Scenario: Branch-dependent cwd
 - **WHEN** one branch changes cwd to `/a` and another changes cwd to `/b`
 - **THEN** a following relative path is not resolved solely under `/a` or solely under `/b`
@@ -272,19 +291,52 @@ rules make it observable.
 - **WHEN** every supported branch exits with the same exact cwd
 - **THEN** the joined cwd remains exact
 
+#### Scenario: Ungated cd failure keeps the prior cwd possible
+- **WHEN** Bash parses `cd /maybe; pwd`
+- **THEN** the `cd` occurrence uses the incoming cwd
+- **THEN** the `pwd` cwd is unknown because `cd` may fail and `;` still continues
+- **THEN** the analyzer does not publish `/maybe` as the sole cwd
+
 #### Scenario: Zero-iteration loop path
 - **WHEN** a loop may execute zero times and its body changes cwd
 - **THEN** the post-loop state includes the pre-loop possibility
 
+#### Scenario: Proved empty loop does not mutate state
+- **WHEN** Bash parses `for f in; do cd /tmp; done; pwd`
+- **THEN** the internal iteration cardinality is `Never`
+- **THEN** the following `pwd` retains the exact incoming cwd
+
+#### Scenario: Duplicate iteration values retain order
+- **WHEN** 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
+- **THEN** the following use of `f` has exact effective value `a`
+
 #### Scenario: Isolated shell scope
 - **WHEN** a supported subshell or scope-isolated group changes cwd
 - **THEN** that cwd does not leak into the enclosing continuation
 
 #### Scenario: Bash substitution cwd is isolated
-- **WHEN** Bash parses `printf '%s' "$(cd /tmp; pwd)"; cat relative.txt`
+- **WHEN** Bash parses `printf '%s' "$(cd /tmp && pwd)"; cat relative.txt`
 - **THEN** `pwd` uses `/tmp` inside the substitution
 - **THEN** `printf` and `cat` retain the exact outer cwd
 
+#### Scenario: Bash last pipeline stage may share parent state
+- **WHEN** a Bash pipeline ends in a cwd or variable-state mutator and parser options do not prove `lastpipe` behavior
+- **THEN** every stage occurrence uses the pipeline input state
+- **THEN** following parent-scope state is unknown when the last stage could run in either a subshell or the current shell
+- **THEN** unproved `pipefail` behavior conservatively partitions every reachable option-dependent result by success and failure
+
+#### Scenario: Decoded Bash wrapper inherits cwd and isolates exit state
+- **WHEN** Bash parses `cd /outer && bash -c 'cd /inner && pwd' && pwd`
+- **THEN** the decoded wrapper enters with exact cwd `/outer`
+- **THEN** its inner `pwd` uses `/inner`
+- **THEN** the following outer `pwd` uses `/outer`
+
+#### Scenario: Decoded Bash wrapper does not inherit an unexported loop binding
+- **WHEN** Bash parses `for f in a; do bash -c 'printf "%s" "$f"'; done`
+- **THEN** the decoded child receives no exact effective `f` from the outer loop binding
+- **THEN** a parenthesized subshell remains distinct because it inherits shell bindings while isolating exit state
+
 #### Scenario: PowerShell subexpression cwd propagates
 - **WHEN** PowerShell parses `Write-Output $(Set-Location /tmp; Get-Location); Get-Item relative.txt`
 - **THEN** `Get-Location`, `Write-Output`, and `Get-Item` use `/tmp`

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

@@ -12,7 +12,12 @@ classification that is false because lexical provenance or consumer/binding
 context was lost. This includes false exact paths, false `Glob` or `Tilde`
 claims, and avoidable `DynamicSkip` results. Every such correction SHALL be
 documented and corpus-pinned; compatibility does not require preserving a
-security defect.
+security defect. When control-flow analysis cannot prove the cwd used by a
+relative compatibility operand, the projection SHALL clear any false exact
+resolution rather than publish one parse-order path as authoritative. It SHALL
+replace any false exact cwd attribution with the existing dynamic cwd marker;
+it SHALL NOT omit the marker and thereby remove a v0.2 consumer's fail-closed
+signal.
 
 #### Scenario: Old consumer sees loop body command
 - **WHEN** Bash fully parses `for f in a b; do rm "$f"; done`
@@ -35,6 +40,13 @@ security defect.
 - **THEN** the compatibility leaf reports the oracle-proved literal path or fails closed
 - **THEN** release notes identify the classification correction
 
+#### Scenario: Joined cwd does not leak a false compatibility path
+- **WHEN** a relative operand may execute under more than one cwd after a loop, pipeline, or conditional list
+- **THEN** its authored spelling, path relevance, and source provenance remain available
+- **THEN** `Arg.Resolved` and the corresponding `ClauseElement.Resolved` are null
+- **THEN** the clause contains a synthetic `<dynamic-cwd>` `DynamicSkip` attribution argument with `Resolved=null`
+- **THEN** no synthetic cwd-attribution argument selects one possible exact path
+
 ### Requirement: Unparseable results are never authorization evidence
 When `ParsedCommand.IsUnparseable=true`, `Commands` and `Clauses` SHALL be
 empty. `Syntax` MAY contain partial diagnostic evidence, and the consumer guide

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

@@ -73,6 +73,10 @@
 - [x] 6.3 Derive exact and finite literal binding domains within the locked candidate cap.
 - [x] 6.4 Substitute a bounded binding only where Bash quoting proves argument boundaries.
 - [ ] 6.5 Propagate and conservatively join cwd and supported binding state across zero-or-more loop execution.
+  - [x] 6.5a Lock outcome-partitioned Bash flow, failure-aware `cd`,
+    conservative `lastpipe` / `pipefail`, ordered iteration plans,
+    decoded-wrapper inheritance, and dynamic fail-closed compatibility
+    sanitization before implementing the state pass.
   - 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

tests/ShellSyntaxTree.Tests/DesignCorpus/V03DesignCorpusTests.cs

@@ -278,6 +278,16 @@ private static void AssertCompatibilityClause(
             Assert.Equal(expected.Element.IsPath, element.IsPath);
             Assert.Equal(expected.Element.Resolved, element.Resolved);
         }
+
+        if (expected.CwdAttribution is not null)
+        {
+            var attribution = Assert.IsType<Arg>(clause.Args[expected.CwdAttribution.ArgumentIndex]);
+            Assert.Equal(expected.CwdAttribution.Raw, attribution.Raw);
+            Assert.Equal(expected.CwdAttribution.Kind, attribution.Kind);
+            Assert.Equal(expected.CwdAttribution.IsPath, attribution.IsPath);
+            Assert.Equal(expected.CwdAttribution.Resolved, attribution.Resolved);
+            Assert.True(attribution.IsCwdAttribution);
+        }
     }
 
     private static void ValidateCompatibilityClauseExpectation(
@@ -316,6 +326,19 @@ private static void ValidateCompatibilityClauseExpectation(
             Assert.False(string.IsNullOrWhiteSpace(expected.Element.Raw));
             Assert.False(string.IsNullOrWhiteSpace(expected.Element.Value));
         }
+
+        if (expected.CwdAttribution is not null)
+        {
+            Assert.NotNull(expected.ArgumentCount);
+            Assert.InRange(
+                expected.CwdAttribution.ArgumentIndex,
+                0,
+                expected.ArgumentCount.Value - 1);
+            Assert.False(string.IsNullOrWhiteSpace(expected.CwdAttribution.Raw));
+            Assert.Equal(ArgKind.DynamicSkip, expected.CwdAttribution.Kind);
+            Assert.False(expected.CwdAttribution.IsPath);
+            Assert.Null(expected.CwdAttribution.Resolved);
+        }
     }
 
     private static void ValidateArgumentExpectation(
@@ -548,6 +571,21 @@ public sealed record CompatibilityClauseExpectation
     public CompatibilityRedirectExpectation? Redirect { get; init; }
 
     public CompatibilityElementExpectation? Element { get; init; }
+
+    public CompatibilityCwdAttributionExpectation? CwdAttribution { get; init; }
+}
+
+public sealed record CompatibilityCwdAttributionExpectation
+{
+    public int ArgumentIndex { get; init; }
+
+    public string Raw { get; init; } = "";
+
+    public ArgKind Kind { get; init; }
+
+    public bool IsPath { get; init; }
+
+    public string? Resolved { get; init; }
 }
 
 public sealed record CompatibilityRedirectExpectation
@@ -638,6 +676,7 @@ public enum DesignSyntaxKind
     ConditionLoop,
     Conditional,
     CommandSubstitution,
+    Group,
     SimpleCommand,
     OpaqueArgument,
     Unsupported,