Implement bounded Bash heredoc analysis

IMPLEMENTATION_PLAN.md

@@ -530,9 +530,21 @@ priorities.
       plus equal-record hash consistency, demonstrate that default JSON is not
       a polymorphic round-trip contract, and make every policy-sensitive
       unknown numeric enum value detectable so consumers can reject it.
-- [ ] Build on the delivered bounded Bash heredoc grammar and quoted-delimiter
-      adjacency by exposing public body/delimiter/expansion/completeness facts,
-      then add a separately tested Bash `<<<` here-string redirect slice.
+- [x] Expose public Bash heredoc body, delimiter, expansion, tab-stripping, and
+      completeness facts from the delivered bounded grammar. Direct tests pin
+      literal and expanding delimiters, every supported substitution command,
+      exact empty/LF/CRLF/tabbed body provenance, the retained v0.2 redirect,
+      and nullable source offsets for decoded `bash -c` payloads.
+- [x] Close the Bash variable-attribute hidden-execution boundary. Named
+      parameter dereferences now require a caller-proved isolated initial
+      state, with that proof propagated into substitutions and subshells.
+      Direct and recursively dispatch-wrapped `eval`, source/dot, trap,
+      variable-attribute and variable-mutating builtins, plus `printf -v`,
+      fail atomically until their state effects are modeled. Native Bash
+      oracles pin nameref-deferred and integer-assignment execution, and the
+      executable corpus carries isolated, unknown-state, and wrapper cases.
+- [ ] Add the separately tested Bash `<<<` here-string redirect slice with
+      bounded operand analysis and trailing-newline semantics.
 
 ---
 

SPEC.md

@@ -280,6 +280,16 @@ mode for every later region that can observe it. In particular, a decoded
 the option is not blindly copied into the child. Cwd-only state changes retain
 the caller's initial-variable assertion.
 
+The same attribute-state proof governs every simple named-parameter
+dereference. With `BashInitialStateMode.Unknown`, `$name` and `${name}` are
+unparseable because an ambient nameref can evaluate an arithmetic array
+subscript and execute authored command text. In isolated mode, a fresh-process
+variable before reachable source mutation may remain an unknown value while
+still being proved free of recursive variable attributes. A modeled ordinary
+loop binding retains its explicit proof. Positional and special parameters
+that cannot carry variable attributes keep their existing typed cardinality
+rules.
+
 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
@@ -791,12 +801,17 @@ 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.
+directory stack is modeled. Unmodeled execution-bearing or
+attribute-mutating builtins fail the complete parse closed globally, not only
+inside loops. The stable catalog is `eval`, `source` / `.`, `trap`, `let`,
+`declare`, `typeset`, `local`, `readonly`, `export`, `unset`, `read`,
+`readarray`, `mapfile`, `getopts`, and `set`, plus `printf -v`. These forms can
+evaluate argument text, install deferred execution, or assign through
+unproved integer, nameref, or array attributes. Recognition recursively
+unwraps statically proved `command` and `builtin` dispatch; dynamic or invalid
+wrapper grammar fails closed. Ordinary `printf` without `-v` remains
+supported. `break`, `continue`, `return`, `exit`, and `exec` remain loop-region
+failures until their transfers are implemented.
 
 Substitutions and subshells inherit the current variable/cwd state but discard
 their state changes on exit. Decoded Bash command wrappers inherit invocation
@@ -1305,17 +1320,20 @@ quoted_string   := single-quoted | double-quoted
 - v0.2 recognizes heredocs (`<<EOF ... EOF`) as redirect syntax while the
   body is skipped. Stable v0.3 preserves delimiter, body, expansion mode,
   tab-stripping mode, and completeness through `HereDocumentAnalysis`.
-  The bounded grammar accepts one terminal `<<` / `<<-` redirect on a command
-  header, with optional whitespace or a trailing comment after the delimiter.
+  The bounded grammar accepts one terminal `<<` / `<<-` redirect, including a
+  literal numeric source descriptor such as `3<<EOF`, on a command header,
+  with optional whitespace or a trailing comment after the delimiter.
   Additional header tokens, pipelines, and queued heredocs are unparseable
   until their body-association grammar is modeled. Quote removal determines
   the delimiter spelling; any quoted or escaped delimiter fragment makes the
   body literal. In an expanding body, unescaped `$()` substitutions are
   executable even when their spelling is surrounded by quote characters,
   because heredoc body quotes are data rather than shell quoting syntax.
-  Escaped substitutions remain literal. Legacy backticks, arithmetic
-  expansion, line continuations that could hide a substitution boundary, and
-  incomplete substitutions make the whole result unparseable.
+  Escaped substitutions remain literal. Legacy backticks, `$((...))` and
+  obsolete `$[...]` arithmetic expansion, prompt-transformed `${name@P}` or
+  other parameter operators, line continuations that could hide a
+  substitution boundary, and incomplete substitutions make the whole result
+  unparseable.
 - Redirect targets matching the POSIX fd-dup / fd-close shorthand —
   `&N`, `&N-`, or `&-` (where `N` is one or more decimal digits) — are
   NOT path-resolved. The parser carries the raw token (e.g. `&1`) on
@@ -1365,6 +1383,9 @@ 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
 substitution is recursively attached to the nearest containing simple command.
+Simple `$name` and `${name}` forms additionally require the proved
+variable-attribute state from §2; syntactic simplicity alone is not evidence
+that dereferencing a nameref cannot execute an array subscript.
 Legacy backtick substitution becomes unparseable in v0.3 until its distinct
 escape and nesting rules can be mapped without guessing. A Bash path-shaped
 glob may produce a `Pattern` only when its exact static covering directory is
@@ -1399,7 +1420,7 @@ The lexer produces tokens consumed by the parser. Token kinds:
   the quote delimiters from the token value. Example: `"hello world"`
   becomes the token value `hello world`.
 - **OPERATOR** — `&&`, `||`, `;`, `|`, `>`, `>>`, `<`, numeric-descriptor
-  forms such as `2>`, `3>>`, and `10<`, `&>`, `&>>`,
+  forms such as `2>`, `3>>`, `10<`, `3<<`, and `4<<-`, `&>`, `&>>`,
   `(`, `)`, `<<`, `<<-`.
 - **WHITESPACE** — one or more spaces, tabs, or newlines (newlines inside
   a heredoc body are not emitted as ordinary tokens; the delimiter token
@@ -1419,9 +1440,9 @@ The lexer produces tokens consumed by the parser. Token kinds:
   Expanding-heredoc substitutions use the same opaque fragment semantics but
   remain attached to the delimiter token rather than entering the ordinary
   command-token stream.
-- **UNPARSEABLE_SENTINEL** — `$((expr))` arithmetic expansion or any
-  operator-bearing parameter expansion such as `${var:-$(cmd)}` or
-  `${var//pat/repl}`. The lexer skips past
+- **UNPARSEABLE_SENTINEL** — `$((expr))` or obsolete `$[expr]` arithmetic
+  expansion, or any operator-bearing parameter expansion such as
+  `${var:-$(cmd)}`, `${var//pat/repl}`, or `${var@P}`. The lexer skips past
   the matching close (`))` or `}` respectively) and emits a sentinel
   whose reason names the rejected construct. The parser consumes this
   token by setting outer `ParsedCommand.IsUnparseable = true` (see §11).
@@ -2307,6 +2328,11 @@ Each file:
 }
 ```
 
+An entry may set `bashInitialStateMode` to `Unknown` or
+`IsolatedNonInteractive` when the expected result depends on the caller-proved
+Bash variable-state contract. When omitted, the Bash corpus runner uses
+`IsolatedNonInteractive`. The field is rejected outside the Bash corpus.
+
 An entry may add an `elements` list to a clause to pin the complete
 `Clause.Elements` projection (`raw`, `value`, `role`, `sourceStart`,
 `sourceLength`, `precedingVerbElementCount`, `kind`, `isFlag`, `isPath`, and

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

@@ -543,6 +543,30 @@ 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.
 
+This state proof applies to every simple Bash parameter dereference, not only
+to loop assignment. A syntactically simple `$name` or `${name}` can execute
+when `name` is a nameref whose target contains an arithmetic array subscript.
+For example, a prior `declare -n x='a[$(hidden)0]'` makes `${x}` evaluate the
+subscript and execute `hidden`, even though the declaration operand was quoted
+data. `Unknown` initial state therefore cannot classify a variable
+dereference as fully accounted for. `IsolatedNonInteractive` may do so only
+before any reachable unmodeled variable mutation, or for a binding whose
+ordinary-scalar attributes are modeled explicitly. The produced value may
+still be `Unknown`; variable-attribute safety and value exactness remain
+independent facts.
+
+Stable v0.3 does not add a partial expression evaluator for Bash builtins.
+Direct or statically wrapped `eval`, `source` / `.`, `trap`, `let`, `declare`,
+`typeset`, `local`, `readonly`, `export`, `unset`, `read`, `readarray`,
+`mapfile`, `getopts`, and `set` forms fail the complete parse closed, as does
+`printf -v`. These commands can execute argument text directly, evaluate
+arithmetic, install deferred execution, or assign through attributes whose
+state is not proved. Exact `command` and `builtin` dispatch wrappers are
+recursively unwrapped; dynamic or invalid wrapper grammar fails closed rather
+than bypassing the catalog. Ordinary `printf` without `-v` remains supported.
+A later additive grammar may admit individually proved query or assignment
+forms without weakening this stable boundary.
+
 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.

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

@@ -29,6 +29,11 @@ fail-closed behavior for incomplete analysis.
 - Add conservative value and shell-state analysis that distinguishes exact,
   finite, bounded-symbolic, and unknown facts without executing commands or
   enumerating the filesystem.
+- Require proved Bash variable-attribute state before treating a simple
+  parameter dereference as non-executable. Stable v0.3 fails closed on
+  unmodeled shell builtins that can evaluate, assign through, or defer
+  argument text, because nameref and arithmetic attributes can otherwise turn
+  quoted data into hidden execution.
 - Preserve resolver-relevant lexical fragments, typed expansion identity and
   cardinality, operation-specific transform eligibility, opaque cause, and
   consumer/binding context through decoding so escaped or

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

@@ -168,6 +168,62 @@ the independently proved variable-state mode.
 - **THEN** the decoded child enters with unknown initial variable state
 - **THEN** the complete result is unparseable rather than publishing an isolated scalar proof
 
+### Requirement: Bash parameter dereferences require proved attribute state
+A syntactically simple Bash `$name` or `${name}` dereference SHALL be treated
+as fully execution-accounted only when the incoming variable-attribute state
+proves that the binding cannot be an integer, nameref, array reference, or
+other recursively evaluated form. Value exactness SHALL remain independent:
+an attribute-safe variable MAY still produce an `Unknown` value.
+
+`BashInitialStateMode.Unknown` SHALL make a simple named-variable dereference
+unparseable because an ambient nameref can evaluate an authored array
+subscript. `IsolatedNonInteractive` MAY establish safe initial attributes for
+a fresh-process variable before reachable source mutation. A modeled ordinary
+loop binding MAY retain that proof. Any reachable unmodeled variable mutation
+SHALL invalidate the proof in later regions that can observe it. Positional
+and special parameters that cannot carry variable attributes remain governed
+by their existing typed cardinality rules.
+
+#### Scenario: Unknown ambient nameref fails closed
+- **WHEN** default-mode Bash parses `printf '%s' "$x"`
+- **THEN** the whole result is unparseable because ambient `x` may be a nameref
+- **THEN** the parser does not report the outer `printf` complete while hiding recursive execution
+
+#### Scenario: Fresh isolated scalar may remain unknown data
+- **WHEN** isolated-mode Bash parses `printf '%s' "$x"` before any source mutation
+- **THEN** the variable value remains unknown
+- **THEN** the dereference does not by itself make the result unparseable because fresh-process attributes are proved safe
+
+#### Scenario: Nameref mutation hides execution in a later heredoc
+- **WHEN** isolated-mode Bash parses `declare -a a; declare -n x='a[$(hidden)0]'; cat <<EOF` followed by `${x}` and `EOF`
+- **THEN** the whole result is unparseable
+- **THEN** no complete heredoc or command projection hides `hidden`
+
+### Requirement: Unmodeled execution-bearing Bash builtins fail closed globally
+Stable v0.3 SHALL fail the complete parse closed for direct or statically
+wrapped Bash builtin forms whose argument text can execute, be evaluated as
+arithmetic, install deferred execution, or assign through unproved variable
+attributes. The bounded catalog SHALL include `eval`, `source` / `.`, `trap`,
+`let`, `declare`, `typeset`, `local`, `readonly`, `export`, `unset`, `read`,
+`readarray`, `mapfile`, `getopts`, and `set`, plus `printf -v`. Exact `command`
+and `builtin` dispatch wrappers SHALL be recursively unwrapped. Dynamic or
+invalid wrapper grammar SHALL fail closed. Ordinary `printf` without `-v`
+SHALL retain its existing behavior.
+
+#### Scenario: Eval payload is not mistaken for inert data
+- **WHEN** Bash parses `eval 'rm target.txt'`
+- **THEN** the whole result is unparseable until eval payload grammar is modeled
+- **THEN** `eval` is not published as a complete occurrence that hides `rm`
+
+#### Scenario: Integer declaration can execute quoted arithmetic data
+- **WHEN** Bash parses `declare -i x='a[$(hidden)0]'`
+- **THEN** the whole result is unparseable
+- **THEN** quoting the assignment operand does not make the builtin evaluation inert
+
+#### Scenario: Exact dispatch wrapper cannot bypass the boundary
+- **WHEN** Bash parses `builtin eval 'rm target.txt'`
+- **THEN** the whole result is unparseable under the same rule as direct `eval`
+
 ### 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,

openspec/changes/v0-3-structured-shell-analysis/specs/explicit-redirect-semantics/spec.md

@@ -130,6 +130,11 @@ executable may interpret that data as code.
 - **THEN** the redirect records that leading tabs are stripped
 - **THEN** authored body provenance remains available
 
+#### Scenario: Numeric-source heredoc
+- **WHEN** Bash parses `cat 3<<EOF` followed by a supported body and delimiter
+- **THEN** descriptor `3`, heredoc operation, delimiter, body, expansion, and completeness facts are preserved
+- **THEN** the numeric descriptor does not cause the body to be tokenized as an ordinary command
+
 ### Requirement: Bash here strings are explicit data redirects
 v0.3 SHALL parse Bash `<<< word` as a `HereString` redirect. Its operand SHALL
 use the normal shell value domain, SHALL NOT be path-relevant, and SHALL account

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

@@ -257,6 +257,11 @@ syntax SHALL be diagnostic evidence only.
 - **WHEN** Bash encounters a single-`&` background list in v0.3
 - **THEN** the whole result is unparseable until concurrency and state boundaries are specified
 
+#### Scenario: Unmodeled execution-bearing Bash builtin
+- **WHEN** Bash encounters a direct or statically dispatch-wrapped builtin whose arguments can execute, defer, or recursively evaluate authored text
+- **THEN** the whole result is unparseable until that builtin's state and execution semantics are modeled
+- **THEN** no complete outer occurrence hides the unmodeled executable region
+
 #### Scenario: Ordinary PowerShell script-block argument
 - **WHEN** PowerShell parses a script block for a canonical receiver proved not to execute that argument
 - **THEN** it remains an opaque dynamic argument